$\forall$$k$, $m$:$\mathbb{N}$. ($\exists$$f$:($\mathbb{N}$$_{\mbox{\scriptsize $<$$k$}}$$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<$$m$}}$). Inj($\mathbb{N}$$_{\mbox{\scriptsize $<$$k$}}$; $\mathbb{N}$$_{\mbox{\scriptsize $<$$m$}}$; $f$)) $\Rightarrow$ $k$$\leq$$m$